#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#include "../model/datatypes.h"
#include "../model/globals.h"
#include "../model/memory_utils.h"
#include "../model/internal_kb.h"
#include "normalized_datatypes.h"
#include "print_utils.h"
#include "globals.h"
#include "locals.h"

NormalizedConcept** normalized_atomic_concepts = NULL;
NormalizedRole** normalized_atomic_roles = NULL;

NormalizedTBox normalized_tbox;


NormalizedConcept* normalize_concept(Concept* c, enum axiom_side side,NormalizedTBox* n_tbox) {
	int i;
	NormalizedConcept* normalized_conjunction;
	NormalizedConcept** conjuncts;
	NormalizedConcept* normalized_atomic_concept;
	NormalizedRole* normalized_atomic_role;
	NormalizedConcept* generated_atomic_concept;
	NormalizedConcept* normalized_filler;

	switch (c->type) {
		case ATOMIC_CONCEPT:
			// atomic concepts in the original TBox are also
			// used in the normalized axioms
			// return (NormalizedConcept*) c;
			normalized_atomic_concept = get_create_normalized_atomic_concept(c);
			return normalized_atomic_concept;
			break;
		case CONJUNCTION:
			conjuncts = (NormalizedConcept**) malloc(c->description.conj->count * sizeof(NormalizedConcept*));
			assert(conjuncts != NULL);
			for (i = 0; i < c->description.conj->count; ++i) {
				conjuncts[i] = normalize_concept(c->description.conj->conjuncts[i], side, n_tbox);
			}
			normalized_conjunction = get_create_normalized_conjunction(conjuncts, c->description.conj->count);
			free(conjuncts);
			return normalized_conjunction;
			break;
		case EXISTENTIAL_RESTRICTION:
			normalized_atomic_role = get_create_normalized_atomic_role(c->description.exists->role);
			if (c->description.exists->filler->type == ATOMIC_CONCEPT) {
				normalized_atomic_concept = get_create_normalized_atomic_concept(c->description.exists->filler);
				// here lookup the concept, if not found create a normalized existential restriction
				return get_create_normalized_exists(normalized_atomic_role,normalized_atomic_concept);
			}
			else {
				normalized_filler = normalize_concept(c->description.exists->filler, side,n_tbox);
				generated_atomic_concept = get_generated_atomic_concept(normalized_filler, side);
				if (generated_atomic_concept == NULL) {
					generated_atomic_concept = create_new_normalized_atomic_concept(side);
					put_generated_atomic_concept(generated_atomic_concept, normalized_filler, side);
					switch (side) {
						case LEFT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(normalized_filler, generated_atomic_concept), n_tbox);
							break;
						case RIGHT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(generated_atomic_concept, normalized_filler), n_tbox);
							break;
						default:
							fprintf(stderr, "axiom side undefined, aborting\n");
							exit(-1);
					}
				}
				return get_create_normalized_exists(normalized_atomic_role, generated_atomic_concept);

			}
			break;
		default:
			fprintf(stderr, "unknown concept type, aborting\n");
			exit(-1);
	}
}

void normalize_subclass_axiom(SubClassAxiom* ax, NormalizedTBox* n_tbox) {
	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->lhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->rhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);
}

void normalize_eqclass_axiom(EqClassAxiom* ax, NormalizedTBox* n_tbox) {

	// create and add 2 subclass axioms
	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->lhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->rhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);

	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->rhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->lhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);

}

void normalize_subrole_axiom(SubRoleAxiom* ax, NormalizedTBox* n_tbox) {
	NormalizedRole* new_role;
	NormalizedRoleComposition* new_composition;

	if (ax->rhs->type != ATOMIC_ROLE) {
		fprintf(stderr,"role compositions on the rhs not supported, aborting!");
		exit(-1);
	}
	switch (ax->lhs->type) {
		case ATOMIC_ROLE:
			add_normalized_axiom(create_normalized_subrole_axiom((NormalizedRole*) ax->lhs, (NormalizedRole*) ax->rhs), n_tbox);
			break;
		case ROLE_COMPOSITION:
			if (ax->lhs->description.role_composition->size == 2) {
				new_role = (NormalizedRole*) malloc(sizeof(NormalizedRole));
				assert(new_role != NULL);	
				new_role->type = NORMALIZED_ROLE_COMPOSITION;

				new_composition = (NormalizedRoleComposition*) malloc(sizeof(NormalizedRoleComposition));
				assert(new_composition != NULL);
				new_composition->role1 = ax->lhs->description.role_composition->roles[0]->description.atomic->id;
				new_composition->role2 = ax->lhs->description.role_composition->roles[1]->description.atomic->id;

				new_role->description.role_comp = new_composition;
			}	
			// TODO:
			else {
				fprintf(stderr, "TODO: subrole axiom normalization!");
			}
			break;
		default:
			fprintf(stderr,"unknown role type, aborting\n");
			exit(-1);

	}
		
}

void normalize_tbox(TBox tbox, NormalizedTBox* n_tbox) {
	int i;

	// init normalized_tbox
	normalized_tbox.axiom_count = 0;
	// axioms will be dynamically added
	normalized_tbox.axioms = NULL;

	// first create space for normalized atomic concepts
	normalized_atomic_concept_count = atomic_concept_count;
	normalized_atomic_concepts = (NormalizedConcept**) malloc(normalized_atomic_concept_count * sizeof(NormalizedConcept*));
	assert(normalized_atomic_concepts != NULL);
	for (i = 0; i < atomic_concept_count; ++i) {
		normalized_atomic_concepts[i] = NULL;
	}

	// now create space for normalized atomic roles
	normalized_atomic_role_count = atomic_role_count;
	normalized_atomic_roles = (NormalizedRole**) malloc(normalized_atomic_role_count * sizeof(NormalizedRole*));
	assert(normalized_atomic_roles != NULL);
	for (i = 0; i < atomic_role_count; ++i) {
		normalized_atomic_roles[i] = NULL;
	}

	for (i = 0; i < tbox.axiom_count; ++i) {
		switch (tbox.axioms[i]->type) {
			case EQCLASS_AX:
				normalize_eqclass_axiom(tbox.axioms[i]->body.eqclass_ax, n_tbox);
				break;
			case SUBCLASS_AX:
				normalize_subclass_axiom(tbox.axioms[i]->body.subclass_ax, n_tbox);
				break;
			case SUBROLE_AX:
				normalize_subrole_axiom(tbox.axioms[i]->body.subrole_ax, n_tbox);
				break;
			default:
				fprintf(stderr, "unknown axiom type, aborting\n");
				exit(-1);
		}
		
	}

}
